$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id. es{-}init{-}state(${\it es}$; $i$) $\in$ es{-}state(${\it es}$; $i$)